A:Realizer, i:Id. R-has-loc(A;i)  R-da(A;i) =   k:Knd fp Type 

latex

Definitions

Id, t  T, s = t, Prop, x:A. B(x), A, Knd, Type, x.A(x), x. t(x), , P  Q, a:A fp B(a), a = b, b, x:AB(x), P  Q, x:AB(x), P & Q, P  Q, {T}, es realizer ind Rrframe compseq tag def, R-da(R;i), R-has-loc(R;i), es realizer ind Rbframe compseq tag def, es realizer ind Raframe compseq tag def, b, , False, Unit, left+right, locl(a), x : v, if b t else f fi, <a,b>, es realizer ind Rpre compseq tag def, source(l), lnk-decl(l;dt), KindDeq, f  g, es realizer ind Rsends compseq tag def, es realizer ind Reffect compseq tag def, es realizer ind Rsframe compseq tag def, es realizer ind Rframe compseq tag def, es realizer ind Rinit compseq tag def, P  Q, p  q, es realizer ind Rplus compseq tag def, es realizer ind Rnone compseq tag def, type List, IdLnk, State(ds), DeclaredType(ds;x), rec(x.A(x)), Realizer, fpf-is-empty(f), Top

Lemmas

fpf-is-empty wf, fpf-join-is-empty, fpf-trivial-subtype-top, top wf, assert of band, assert-fpf-is-empty, es realizer wf, unit wf, decl-type wf, decl-state wf, IdLnk wf, false wf, assert of bor, bor wf, R-da wf, R-has-loc wf, fpf-join wf, lnk-decl wf, Kind-deq wf, lsrc wf, ifthenelse wf, fpf-single wf, locl wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, bool wf, bnot wf, all functionality wrt iff, implies functionality wrt iff, not functionality wrt iff, assert-eq-id, assert wf, eq id wf, fpf wf, fpf-empty wf, Knd wf, not wf, Id wf